;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ihuechange
  (sig pixel-to-hue (col r g b h))
  (sig make-hue-columns (row columns hue))
  (sig pixel-to-hue-original (r g b h))
  (sig hue-change (tree hue))
  
  ; pixel-to-hue returns a list of 4 numbers:
  ; the column number followed by three numbers between [0, 255]
  (con pixel-to-hue-returns-list-of-4
       (implies (and (and (natp r) (<= r 255))
                     (and (natp g) (<= g 255))
                     (and (natp b) (<= b 255))
                     (and (natp hue) (<= hue 360))
                     (natp col))
                (let* ((newRGB (pixel-to-hue col r g b hue))
                       (newR   (cadr newRGB))
                       (newG   (caddr newRGB))
                       (newB   (cadddr newRGB)))
                  (and (= (len newRGB) 4)
                       (and (natp newR) (<= newR 255))
                       (and (natp newG) (<= newG 255))
                       (and (natp newB) (<= newB 255))))))
       
  ; The hue-change function returns a tree.
  (con hue-change-returns-tree
       (implies (and (bmp-tree? tr)
                     (and (napt hue) (<= hue 360)))
                (bmp-tree? (hue-change tr hue)))))